Nuprl Lemma : split_tail_wf
4,23
postcript
pdf
A
:Type,
f
:(
A
),
L
:
A
List. split_tail(
L
|
x
.
f
(
x
))
(
A
List)
(
A
List)
latex
Definitions
t
T
,
x
(
s
)
,
x
:
A
.
B
(
x
)
,
if
b
t
else
f
fi
,
,
split_tail(
L
|
x
.
f
(
x
))
Lemmas
bool
wf
,
ifthenelse
wf
origin
A:Type, f:(A
), L:A List. split_tail(L | x.f(x)) 
(A List)
(A List) A:Type, f:(A), L:A List. split_tail(L | x.f(x)) (A List)(A List) Tx:A. B(x)
t else f fix.f(x))